/*
 * InplaceNNFProcessorTest.cpp
 *
 *  Created on: Dec 17, 2009
 *      Author: anton.kuhlevskyi
 */

#include <gtest/gtest.h>
#include <gmock/gmock.h>

#include <memory>

// Tested file
#include "Processors/NNF/Inplace.h"

#include "Nodes/Binary/Node.h"
#include "Parsers/PostfixParser.h"
#include "Printers/PostfixPrinter.h"

TEST(InplaceNNFProcessorTest, NotAnd)
{
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory);

	// Check processing of ~(A & B) -> ~A | ~B
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB&~", factory));

	BinaryNode* pA = node->getChild(0)->getChild(0);
	BinaryNode* pB = node->getChild(0)->getChild(1);

	EXPECT_TRUE(processor(node));
	EXPECT_EQ("A~B~|", PostfixPrinter<BinaryNode>::print(node.get()));
	EXPECT_EQ(pA, node->getChild(0)->getChild(0));
	EXPECT_EQ(pB, node->getChild(1)->getChild(0));
}

TEST(InplaceNNFProcessorTest, NotOr)
{
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory);

	// Check processing of ~(A | B) -> ~A & ~B
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB|~", factory));

	BinaryNode* pA = node->getChild(0)->getChild(0);
	BinaryNode* pB = node->getChild(0)->getChild(1);

	EXPECT_TRUE(processor(node));
	EXPECT_EQ("A~B~&", PostfixPrinter<BinaryNode>::print(node.get()));
	EXPECT_EQ(pA, node->getChild(0)->getChild(0));
	EXPECT_EQ(pB, node->getChild(1)->getChild(0));
}

TEST(InplaceNNFProcessorTest, NotNot)
{
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory);

	// Check processing of ~~A -> A
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("A~~", factory));

	BinaryNode* pA = node->getChild(0)->getChild(0);

	EXPECT_TRUE(processor(node));
	EXPECT_EQ("A", PostfixPrinter<BinaryNode>::print(node.get()));
	EXPECT_EQ(pA, node.get());
}

TEST(InplaceNNFProcessorTest, MatchOrAnd1)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory);

	// Check processing of (A & B) | C -> (A & C) | (B & C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB&C|", factory));

	BinaryNode* pOr = node.get();
	BinaryNode* pAnd = node->getChild(0);
	BinaryNode* pA = node->getChild(0)->getChild(0);
	BinaryNode* pB = node->getChild(0)->getChild(1);
	BinaryNode* pC = node->getChild(1);

	EXPECT_TRUE(processor(node));
	EXPECT_EQ("AC&BC&|", PostfixPrinter<BinaryNode>::print(node.get()));

	EXPECT_EQ(pOr, node.get());
	EXPECT_TRUE((pAnd==node->getChild(0)) || (pAnd==node->getChild(1)));

	EXPECT_EQ(pA, node->getChild(0)->getChild(0));
	EXPECT_EQ(pB, node->getChild(1)->getChild(0));
	EXPECT_TRUE((pC==node->getChild(0)->getChild(1))
				|| (pC==node->getChild(1)->getChild(1)));
}

TEST(InplaceNNFProcessorTest, MatchOrAnd2)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory);

	// Check processing of A | (B & C) -> (A & B) | (A & C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("ABC&|", factory));

	BinaryNode* pOr		= node.get();
	BinaryNode* pAnd	= node->getChild(1);
	BinaryNode* pA		= node->getChild(0);
	BinaryNode* pB		= node->getChild(1)->getChild(0);
	BinaryNode* pC 		= node->getChild(1)->getChild(1);

	EXPECT_TRUE(processor(node));
	EXPECT_EQ("AB&AC&|", PostfixPrinter<BinaryNode>::print(node.get()));

	EXPECT_EQ(pOr, node.get());
	EXPECT_TRUE((pAnd==node->getChild(0)) || (pAnd==node->getChild(1)));

	EXPECT_TRUE((pA==node->getChild(0)->getChild(0))
					|| (pA==node->getChild(1)->getChild(0)));
	EXPECT_EQ(pB, node->getChild(0)->getChild(1));
	EXPECT_EQ(pC, node->getChild(1)->getChild(1));

}

TEST(InplaceNNFProcessorTest, AndOr1)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory, CNF);

	// Check processing of (A | B) & C -> (A | C) & (B | C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB|C&", factory));

	BinaryNode* pAnd	= node.get();
	BinaryNode* pOr		= node->getChild(0);
	BinaryNode* pA		= node->getChild(0)->getChild(0);
	BinaryNode* pB		= node->getChild(0)->getChild(1);
	BinaryNode* pC 		= node->getChild(1);

	EXPECT_TRUE(processor(node));
	EXPECT_EQ("AC|BC|&", PostfixPrinter<BinaryNode>::print(node.get()));

	EXPECT_EQ(pAnd, node.get());
	EXPECT_TRUE((pOr==node->getChild(0)) || (pOr==node->getChild(1)));

	EXPECT_EQ(pA, node->getChild(0)->getChild(0));
	EXPECT_EQ(pB, node->getChild(1)->getChild(0));
	EXPECT_TRUE((pC==node->getChild(0)->getChild(1))
				|| (pC==node->getChild(1)->getChild(1)));
}

TEST(InplaceNNFProcessorTest, AndOr2)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory, CNF);

	// Check processing of A & (B | C) -> (A | B) & (A | C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("ABC|&", factory));

	BinaryNode* pAnd		= node.get();
	BinaryNode* pOr	= node->getChild(1);
	BinaryNode* pA		= node->getChild(0);
	BinaryNode* pB		= node->getChild(1)->getChild(0);
	BinaryNode* pC 		= node->getChild(1)->getChild(1);

	EXPECT_TRUE(processor(node));
	EXPECT_EQ("AB|AC|&", PostfixPrinter<BinaryNode>::print(node.get()));

	EXPECT_EQ(pAnd, node.get());
	EXPECT_TRUE((pOr==node->getChild(0)) || (pOr==node->getChild(1)));

	EXPECT_TRUE((pA==node->getChild(0)->getChild(0))
					|| (pA==node->getChild(1)->getChild(0)));
	EXPECT_EQ(pB, node->getChild(0)->getChild(1));
	EXPECT_EQ(pC, node->getChild(1)->getChild(1));
}

TEST(InplaceNNFProcessorTest, AndOrNotAppliedInDNFMode)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory, DNF);

	// Check processing of A & (B | C) -> (A | B) & (A | C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("ABC|&", factory));
	EXPECT_FALSE(processor(node));

	// Check processing of A & (B | C) -> (A | B) & (A | C)
	node.reset(postfixParse<BinaryNode>("ABC|&", factory));
	EXPECT_FALSE(processor(node));
}

TEST(InplaceNNFProcessorTest, MatchOrAndNotAppliedInDNFMode)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	InplaceNNFProcessor< BinaryNode , NodeFactory<BinaryNode> > processor(factory, CNF);

	// Check processing of (A & B) | C -> (A & C) | (B & C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB&C|", factory));

	EXPECT_FALSE(processor(node));

	// Check processing of A | (B & C) -> (A & B) | (A & C)
	node.reset(postfixParse<BinaryNode>("ABC&|", factory));

	EXPECT_FALSE(processor(node));
}
